Left Termination of the query pattern reach_in_4(g, g, g, g) w.r.t. the given Prolog program could not be shown:



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof

Clauses:

reach(X, Y, Edges, Visited) :- member(.(X, .(Y, [])), Edges).
reach(X, Z, Edges, Visited) :- ','(member1(.(X, .(Y, [])), Edges), ','(member(Y, Visited), reach(Y, Z, Edges, .(Y, Visited)))).
member(H, .(H, L)).
member(X, .(H, L)) :- member(X, L).
member1(H, .(H, L)).
member1(X, .(H, L)) :- member1(X, L).

Queries:

reach(g,g,g,g).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
reach_in: (b,b,b,b) (f,b,b,b)
member_in: (b,b) (f,b)
member1_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x5)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

REACH_IN_GGGG(X, Y, Edges, Visited) → U1_GGGG(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_GGGG(X, Y, Edges, Visited) → MEMBER_IN_GG(.(X, .(Y, [])), Edges)
MEMBER_IN_GG(X, .(H, L)) → U5_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
REACH_IN_GGGG(X, Z, Edges, Visited) → U2_GGGG(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_GGGG(X, Z, Edges, Visited) → MEMBER1_IN_GG(.(X, .(Y, [])), Edges)
MEMBER1_IN_GG(X, .(H, L)) → U6_GG(X, H, L, member1_in_gg(X, L))
MEMBER1_IN_GG(X, .(H, L)) → MEMBER1_IN_GG(X, L)
U2_GGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_GGGG(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U2_GGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → MEMBER_IN_AG(Y, Visited)
MEMBER_IN_AG(X, .(H, L)) → U5_AG(X, H, L, member_in_ag(X, L))
MEMBER_IN_AG(X, .(H, L)) → MEMBER_IN_AG(X, L)
U3_GGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_GGGG(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U3_GGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → REACH_IN_AGGG(Y, Z, Edges, .(Y, Visited))
REACH_IN_AGGG(X, Y, Edges, Visited) → U1_AGGG(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_AGGG(X, Y, Edges, Visited) → MEMBER_IN_GG(.(X, .(Y, [])), Edges)
REACH_IN_AGGG(X, Z, Edges, Visited) → U2_AGGG(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_AGGG(X, Z, Edges, Visited) → MEMBER1_IN_GG(.(X, .(Y, [])), Edges)
U2_AGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_AGGG(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U2_AGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → MEMBER_IN_AG(Y, Visited)
U3_AGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_AGGG(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U3_AGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → REACH_IN_AGGG(Y, Z, Edges, .(Y, Visited))

The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x5)
U2_GGGG(x1, x2, x3, x4, x5)  =  U2_GGGG(x2, x3, x4, x5)
U6_GG(x1, x2, x3, x4)  =  U6_GG(x4)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)
MEMBER1_IN_GG(x1, x2)  =  MEMBER1_IN_GG(x1, x2)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
REACH_IN_GGGG(x1, x2, x3, x4)  =  REACH_IN_GGGG(x1, x2, x3, x4)
U1_GGGG(x1, x2, x3, x4, x5)  =  U1_GGGG(x5)
U3_GGGG(x1, x2, x3, x4, x5, x6)  =  U3_GGGG(x2, x3, x4, x6)
U4_GGGG(x1, x2, x3, x4, x5)  =  U4_GGGG(x5)
U3_AGGG(x1, x2, x3, x4, x5, x6)  =  U3_AGGG(x2, x3, x4, x6)
U5_GG(x1, x2, x3, x4)  =  U5_GG(x4)
U4_AGGG(x1, x2, x3, x4, x5)  =  U4_AGGG(x5)
U1_AGGG(x1, x2, x3, x4, x5)  =  U1_AGGG(x5)
REACH_IN_AGGG(x1, x2, x3, x4)  =  REACH_IN_AGGG(x2, x3, x4)
U5_AG(x1, x2, x3, x4)  =  U5_AG(x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

REACH_IN_GGGG(X, Y, Edges, Visited) → U1_GGGG(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_GGGG(X, Y, Edges, Visited) → MEMBER_IN_GG(.(X, .(Y, [])), Edges)
MEMBER_IN_GG(X, .(H, L)) → U5_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
REACH_IN_GGGG(X, Z, Edges, Visited) → U2_GGGG(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_GGGG(X, Z, Edges, Visited) → MEMBER1_IN_GG(.(X, .(Y, [])), Edges)
MEMBER1_IN_GG(X, .(H, L)) → U6_GG(X, H, L, member1_in_gg(X, L))
MEMBER1_IN_GG(X, .(H, L)) → MEMBER1_IN_GG(X, L)
U2_GGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_GGGG(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U2_GGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → MEMBER_IN_AG(Y, Visited)
MEMBER_IN_AG(X, .(H, L)) → U5_AG(X, H, L, member_in_ag(X, L))
MEMBER_IN_AG(X, .(H, L)) → MEMBER_IN_AG(X, L)
U3_GGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_GGGG(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U3_GGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → REACH_IN_AGGG(Y, Z, Edges, .(Y, Visited))
REACH_IN_AGGG(X, Y, Edges, Visited) → U1_AGGG(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_AGGG(X, Y, Edges, Visited) → MEMBER_IN_GG(.(X, .(Y, [])), Edges)
REACH_IN_AGGG(X, Z, Edges, Visited) → U2_AGGG(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_AGGG(X, Z, Edges, Visited) → MEMBER1_IN_GG(.(X, .(Y, [])), Edges)
U2_AGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_AGGG(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U2_AGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → MEMBER_IN_AG(Y, Visited)
U3_AGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_AGGG(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U3_AGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → REACH_IN_AGGG(Y, Z, Edges, .(Y, Visited))

The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x5)
U2_GGGG(x1, x2, x3, x4, x5)  =  U2_GGGG(x2, x3, x4, x5)
U6_GG(x1, x2, x3, x4)  =  U6_GG(x4)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)
MEMBER1_IN_GG(x1, x2)  =  MEMBER1_IN_GG(x1, x2)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
REACH_IN_GGGG(x1, x2, x3, x4)  =  REACH_IN_GGGG(x1, x2, x3, x4)
U1_GGGG(x1, x2, x3, x4, x5)  =  U1_GGGG(x5)
U3_GGGG(x1, x2, x3, x4, x5, x6)  =  U3_GGGG(x2, x3, x4, x6)
U4_GGGG(x1, x2, x3, x4, x5)  =  U4_GGGG(x5)
U3_AGGG(x1, x2, x3, x4, x5, x6)  =  U3_AGGG(x2, x3, x4, x6)
U5_GG(x1, x2, x3, x4)  =  U5_GG(x4)
U4_AGGG(x1, x2, x3, x4, x5)  =  U4_AGGG(x5)
U1_AGGG(x1, x2, x3, x4, x5)  =  U1_AGGG(x5)
REACH_IN_AGGG(x1, x2, x3, x4)  =  REACH_IN_AGGG(x2, x3, x4)
U5_AG(x1, x2, x3, x4)  =  U5_AG(x4)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 4 SCCs with 16 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_AG(X, .(H, L)) → MEMBER_IN_AG(X, L)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x5)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_AG(X, .(H, L)) → MEMBER_IN_AG(X, L)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

MEMBER_IN_AG(.(L)) → MEMBER_IN_AG(L)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

MEMBER1_IN_GG(X, .(H, L)) → MEMBER1_IN_GG(X, L)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x5)
MEMBER1_IN_GG(x1, x2)  =  MEMBER1_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

MEMBER1_IN_GG(X, .(H, L)) → MEMBER1_IN_GG(X, L)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
MEMBER1_IN_GG(x1, x2)  =  MEMBER1_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

MEMBER1_IN_GG(X, .(L)) → MEMBER1_IN_GG(X, L)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x5)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(L)) → MEMBER_IN_GG(X, L)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U3_AGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → REACH_IN_AGGG(Y, Z, Edges, .(Y, Visited))
REACH_IN_AGGG(X, Z, Edges, Visited) → U2_AGGG(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_AGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_AGGG(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))

The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x5)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
U3_AGGG(x1, x2, x3, x4, x5, x6)  =  U3_AGGG(x2, x3, x4, x6)
REACH_IN_AGGG(x1, x2, x3, x4)  =  REACH_IN_AGGG(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U3_AGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → REACH_IN_AGGG(Y, Z, Edges, .(Y, Visited))
REACH_IN_AGGG(X, Z, Edges, Visited) → U2_AGGG(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_AGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_AGGG(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))

The TRS R consists of the following rules:

member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
[]  =  []
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
U3_AGGG(x1, x2, x3, x4, x5, x6)  =  U3_AGGG(x2, x3, x4, x6)
REACH_IN_AGGG(x1, x2, x3, x4)  =  REACH_IN_AGGG(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

REACH_IN_AGGG(Z, Edges, Visited) → U2_AGGG(Z, Edges, Visited, member1_in_gg(.(.([])), Edges))
U2_AGGG(Z, Edges, Visited, member1_out_gg) → U3_AGGG(Z, Edges, Visited, member_in_ag(Visited))
U3_AGGG(Z, Edges, Visited, member_out_ag) → REACH_IN_AGGG(Z, Edges, .(Visited))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U6_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U5_ag(member_in_ag(L))
U6_gg(member1_out_gg) → member1_out_gg
U5_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule REACH_IN_AGGG(Z, Edges, Visited) → U2_AGGG(Z, Edges, Visited, member1_in_gg(.(.([])), Edges)) at position [3] we obtained the following new rules:

REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, member1_out_gg)
REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, U6_gg(member1_in_gg(.(.([])), x1)))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U2_AGGG(Z, Edges, Visited, member1_out_gg) → U3_AGGG(Z, Edges, Visited, member_in_ag(Visited))
REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, member1_out_gg)
U3_AGGG(Z, Edges, Visited, member_out_ag) → REACH_IN_AGGG(Z, Edges, .(Visited))
REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, U6_gg(member1_in_gg(.(.([])), x1)))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U6_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U5_ag(member_in_ag(L))
U6_gg(member1_out_gg) → member1_out_gg
U5_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule U2_AGGG(Z, Edges, Visited, member1_out_gg) → U3_AGGG(Z, Edges, Visited, member_in_ag(Visited)) at position [3] we obtained the following new rules:

U2_AGGG(y0, y1, .(x0), member1_out_gg) → U3_AGGG(y0, y1, .(x0), U5_ag(member_in_ag(x0)))
U2_AGGG(y0, y1, .(x0), member1_out_gg) → U3_AGGG(y0, y1, .(x0), member_out_ag)



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U2_AGGG(y0, y1, .(x0), member1_out_gg) → U3_AGGG(y0, y1, .(x0), member_out_ag)
REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, member1_out_gg)
U2_AGGG(y0, y1, .(x0), member1_out_gg) → U3_AGGG(y0, y1, .(x0), U5_ag(member_in_ag(x0)))
U3_AGGG(Z, Edges, Visited, member_out_ag) → REACH_IN_AGGG(Z, Edges, .(Visited))
REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, U6_gg(member1_in_gg(.(.([])), x1)))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U6_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U5_ag(member_in_ag(L))
U6_gg(member1_out_gg) → member1_out_gg
U5_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U3_AGGG(Z, Edges, Visited, member_out_ag) → REACH_IN_AGGG(Z, Edges, .(Visited)) we obtained the following new rules:

U3_AGGG(z0, z1, .(z2), member_out_ag) → REACH_IN_AGGG(z0, z1, .(.(z2)))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U2_AGGG(y0, y1, .(x0), member1_out_gg) → U3_AGGG(y0, y1, .(x0), member_out_ag)
REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, member1_out_gg)
U2_AGGG(y0, y1, .(x0), member1_out_gg) → U3_AGGG(y0, y1, .(x0), U5_ag(member_in_ag(x0)))
U3_AGGG(z0, z1, .(z2), member_out_ag) → REACH_IN_AGGG(z0, z1, .(.(z2)))
REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, U6_gg(member1_in_gg(.(.([])), x1)))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U6_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U5_ag(member_in_ag(L))
U6_gg(member1_out_gg) → member1_out_gg
U5_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, member1_out_gg) we obtained the following new rules:

REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), member1_out_gg)



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), member1_out_gg)
U2_AGGG(y0, y1, .(x0), member1_out_gg) → U3_AGGG(y0, y1, .(x0), member_out_ag)
U2_AGGG(y0, y1, .(x0), member1_out_gg) → U3_AGGG(y0, y1, .(x0), U5_ag(member_in_ag(x0)))
U3_AGGG(z0, z1, .(z2), member_out_ag) → REACH_IN_AGGG(z0, z1, .(.(z2)))
REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, U6_gg(member1_in_gg(.(.([])), x1)))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U6_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U5_ag(member_in_ag(L))
U6_gg(member1_out_gg) → member1_out_gg
U5_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, U6_gg(member1_in_gg(.(.([])), x1))) we obtained the following new rules:

REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), U6_gg(member1_in_gg(.(.([])), x1)))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), member1_out_gg)
REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), U6_gg(member1_in_gg(.(.([])), x1)))
U2_AGGG(y0, y1, .(x0), member1_out_gg) → U3_AGGG(y0, y1, .(x0), member_out_ag)
U2_AGGG(y0, y1, .(x0), member1_out_gg) → U3_AGGG(y0, y1, .(x0), U5_ag(member_in_ag(x0)))
U3_AGGG(z0, z1, .(z2), member_out_ag) → REACH_IN_AGGG(z0, z1, .(.(z2)))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U6_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U5_ag(member_in_ag(L))
U6_gg(member1_out_gg) → member1_out_gg
U5_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U2_AGGG(y0, y1, .(x0), member1_out_gg) → U3_AGGG(y0, y1, .(x0), U5_ag(member_in_ag(x0))) we obtained the following new rules:

U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(z2)), U5_ag(member_in_ag(.(z2))))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
                                              ↳ QDP
                                                ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), member1_out_gg)
REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), U6_gg(member1_in_gg(.(.([])), x1)))
U2_AGGG(y0, y1, .(x0), member1_out_gg) → U3_AGGG(y0, y1, .(x0), member_out_ag)
U3_AGGG(z0, z1, .(z2), member_out_ag) → REACH_IN_AGGG(z0, z1, .(.(z2)))
U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(z2)), U5_ag(member_in_ag(.(z2))))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U6_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U5_ag(member_in_ag(L))
U6_gg(member1_out_gg) → member1_out_gg
U5_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U2_AGGG(y0, y1, .(x0), member1_out_gg) → U3_AGGG(y0, y1, .(x0), member_out_ag) we obtained the following new rules:

U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag)



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
                                              ↳ QDP
                                                ↳ Instantiation
                                                  ↳ QDP
                                                    ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), member1_out_gg)
REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), U6_gg(member1_in_gg(.(.([])), x1)))
U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag)
U3_AGGG(z0, z1, .(z2), member_out_ag) → REACH_IN_AGGG(z0, z1, .(.(z2)))
U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(z2)), U5_ag(member_in_ag(.(z2))))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U6_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U5_ag(member_in_ag(L))
U6_gg(member1_out_gg) → member1_out_gg
U5_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U3_AGGG(z0, z1, .(z2), member_out_ag) → REACH_IN_AGGG(z0, z1, .(.(z2))) we obtained the following new rules:

U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag) → REACH_IN_AGGG(z0, .(z1), .(.(.(z2))))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
                                              ↳ QDP
                                                ↳ Instantiation
                                                  ↳ QDP
                                                    ↳ Instantiation
                                                      ↳ QDP
                                                        ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), member1_out_gg)
REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), U6_gg(member1_in_gg(.(.([])), x1)))
U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag) → REACH_IN_AGGG(z0, .(z1), .(.(.(z2))))
U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag)
U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(z2)), U5_ag(member_in_ag(.(z2))))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U6_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U5_ag(member_in_ag(L))
U6_gg(member1_out_gg) → member1_out_gg
U5_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), member1_out_gg) we obtained the following new rules:

REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg)



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
                                              ↳ QDP
                                                ↳ Instantiation
                                                  ↳ QDP
                                                    ↳ Instantiation
                                                      ↳ QDP
                                                        ↳ Instantiation
                                                          ↳ QDP
                                                            ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), U6_gg(member1_in_gg(.(.([])), x1)))
U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag)
U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag) → REACH_IN_AGGG(z0, .(z1), .(.(.(z2))))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg)
U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(z2)), U5_ag(member_in_ag(.(z2))))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U6_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U5_ag(member_in_ag(L))
U6_gg(member1_out_gg) → member1_out_gg
U5_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), U6_gg(member1_in_gg(.(.([])), x1))) we obtained the following new rules:

REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), U6_gg(member1_in_gg(.(.([])), z1)))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
                                              ↳ QDP
                                                ↳ Instantiation
                                                  ↳ QDP
                                                    ↳ Instantiation
                                                      ↳ QDP
                                                        ↳ Instantiation
                                                          ↳ QDP
                                                            ↳ Instantiation
                                                              ↳ QDP
                                                                ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag) → REACH_IN_AGGG(z0, .(z1), .(.(.(z2))))
U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag)
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), U6_gg(member1_in_gg(.(.([])), z1)))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg)
U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(z2)), U5_ag(member_in_ag(.(z2))))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U6_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U5_ag(member_in_ag(L))
U6_gg(member1_out_gg) → member1_out_gg
U5_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(z2)), U5_ag(member_in_ag(.(z2)))) we obtained the following new rules:

U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(.(z2))), U5_ag(member_in_ag(.(.(z2)))))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
                                              ↳ QDP
                                                ↳ Instantiation
                                                  ↳ QDP
                                                    ↳ Instantiation
                                                      ↳ QDP
                                                        ↳ Instantiation
                                                          ↳ QDP
                                                            ↳ Instantiation
                                                              ↳ QDP
                                                                ↳ Instantiation
                                                                  ↳ QDP
                                                                    ↳ Instantiation
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag)
U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag) → REACH_IN_AGGG(z0, .(z1), .(.(.(z2))))
U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(.(z2))), U5_ag(member_in_ag(.(.(z2)))))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), U6_gg(member1_in_gg(.(.([])), z1)))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg)

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U6_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U5_ag(member_in_ag(L))
U6_gg(member1_out_gg) → member1_out_gg
U5_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag) we obtained the following new rules:

U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(.(z2))), member_out_ag)



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
                                              ↳ QDP
                                                ↳ Instantiation
                                                  ↳ QDP
                                                    ↳ Instantiation
                                                      ↳ QDP
                                                        ↳ Instantiation
                                                          ↳ QDP
                                                            ↳ Instantiation
                                                              ↳ QDP
                                                                ↳ Instantiation
                                                                  ↳ QDP
                                                                    ↳ Instantiation
                                                                      ↳ QDP
                                                                        ↳ NonTerminationProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag) → REACH_IN_AGGG(z0, .(z1), .(.(.(z2))))
U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(.(z2))), member_out_ag)
U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(.(z2))), U5_ag(member_in_ag(.(.(z2)))))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), U6_gg(member1_in_gg(.(.([])), z1)))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg)

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U6_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U5_ag(member_in_ag(L))
U6_gg(member1_out_gg) → member1_out_gg
U5_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)

We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag) → REACH_IN_AGGG(z0, .(z1), .(.(.(z2))))
U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(.(z2))), member_out_ag)
U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(.(z2))), U5_ag(member_in_ag(.(.(z2)))))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), U6_gg(member1_in_gg(.(.([])), z1)))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg)

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U6_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U5_ag(member_in_ag(L))
U6_gg(member1_out_gg) → member1_out_gg
U5_ag(member_out_ag) → member_out_ag


s = REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) evaluates to t =REACH_IN_AGGG(z0, .(z1), .(.(.(.(z2)))))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg)
with rule REACH_IN_AGGG(z0', .(z1'), .(.(.(z2')))) → U2_AGGG(z0', .(z1'), .(.(.(z2'))), member1_out_gg) at position [] and matcher [z1' / z1, z2' / z2, z0' / z0]

U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg) → U3_AGGG(z0, .(z1), .(.(.(z2))), member_out_ag)
with rule U2_AGGG(z0', .(z1'), .(.(.(z2'))), member1_out_gg) → U3_AGGG(z0', .(z1'), .(.(.(z2'))), member_out_ag) at position [] and matcher [z1' / z1, z2' / z2, z0' / z0]

U3_AGGG(z0, .(z1), .(.(.(z2))), member_out_ag) → REACH_IN_AGGG(z0, .(z1), .(.(.(.(z2)))))
with rule U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag) → REACH_IN_AGGG(z0, .(z1), .(.(.(z2))))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.




We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
reach_in: (b,b,b,b) (f,b,b,b)
member_in: (b,b) (f,b)
member1_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x1, x2, x3, x4, x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x3, x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg(x1, x2)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x1, x3, x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x1, x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x2, x3, x4, x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x2, x3, x4, x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x1, x2, x3, x4, x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x3, x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg(x1, x2)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x1, x3, x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x1, x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x2, x3, x4, x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x2, x3, x4, x5)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

REACH_IN_GGGG(X, Y, Edges, Visited) → U1_GGGG(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_GGGG(X, Y, Edges, Visited) → MEMBER_IN_GG(.(X, .(Y, [])), Edges)
MEMBER_IN_GG(X, .(H, L)) → U5_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
REACH_IN_GGGG(X, Z, Edges, Visited) → U2_GGGG(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_GGGG(X, Z, Edges, Visited) → MEMBER1_IN_GG(.(X, .(Y, [])), Edges)
MEMBER1_IN_GG(X, .(H, L)) → U6_GG(X, H, L, member1_in_gg(X, L))
MEMBER1_IN_GG(X, .(H, L)) → MEMBER1_IN_GG(X, L)
U2_GGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_GGGG(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U2_GGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → MEMBER_IN_AG(Y, Visited)
MEMBER_IN_AG(X, .(H, L)) → U5_AG(X, H, L, member_in_ag(X, L))
MEMBER_IN_AG(X, .(H, L)) → MEMBER_IN_AG(X, L)
U3_GGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_GGGG(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U3_GGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → REACH_IN_AGGG(Y, Z, Edges, .(Y, Visited))
REACH_IN_AGGG(X, Y, Edges, Visited) → U1_AGGG(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_AGGG(X, Y, Edges, Visited) → MEMBER_IN_GG(.(X, .(Y, [])), Edges)
REACH_IN_AGGG(X, Z, Edges, Visited) → U2_AGGG(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_AGGG(X, Z, Edges, Visited) → MEMBER1_IN_GG(.(X, .(Y, [])), Edges)
U2_AGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_AGGG(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U2_AGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → MEMBER_IN_AG(Y, Visited)
U3_AGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_AGGG(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U3_AGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → REACH_IN_AGGG(Y, Z, Edges, .(Y, Visited))

The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x1, x2, x3, x4, x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x3, x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg(x1, x2)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x1, x3, x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x1, x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x2, x3, x4, x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x2, x3, x4, x5)
U2_GGGG(x1, x2, x3, x4, x5)  =  U2_GGGG(x1, x2, x3, x4, x5)
U6_GG(x1, x2, x3, x4)  =  U6_GG(x1, x3, x4)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)
MEMBER1_IN_GG(x1, x2)  =  MEMBER1_IN_GG(x1, x2)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
REACH_IN_GGGG(x1, x2, x3, x4)  =  REACH_IN_GGGG(x1, x2, x3, x4)
U1_GGGG(x1, x2, x3, x4, x5)  =  U1_GGGG(x1, x2, x3, x4, x5)
U3_GGGG(x1, x2, x3, x4, x5, x6)  =  U3_GGGG(x1, x2, x3, x4, x6)
U4_GGGG(x1, x2, x3, x4, x5)  =  U4_GGGG(x1, x2, x3, x4, x5)
U3_AGGG(x1, x2, x3, x4, x5, x6)  =  U3_AGGG(x2, x3, x4, x6)
U5_GG(x1, x2, x3, x4)  =  U5_GG(x1, x3, x4)
U4_AGGG(x1, x2, x3, x4, x5)  =  U4_AGGG(x2, x3, x4, x5)
U1_AGGG(x1, x2, x3, x4, x5)  =  U1_AGGG(x2, x3, x4, x5)
REACH_IN_AGGG(x1, x2, x3, x4)  =  REACH_IN_AGGG(x2, x3, x4)
U5_AG(x1, x2, x3, x4)  =  U5_AG(x3, x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

REACH_IN_GGGG(X, Y, Edges, Visited) → U1_GGGG(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_GGGG(X, Y, Edges, Visited) → MEMBER_IN_GG(.(X, .(Y, [])), Edges)
MEMBER_IN_GG(X, .(H, L)) → U5_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
REACH_IN_GGGG(X, Z, Edges, Visited) → U2_GGGG(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_GGGG(X, Z, Edges, Visited) → MEMBER1_IN_GG(.(X, .(Y, [])), Edges)
MEMBER1_IN_GG(X, .(H, L)) → U6_GG(X, H, L, member1_in_gg(X, L))
MEMBER1_IN_GG(X, .(H, L)) → MEMBER1_IN_GG(X, L)
U2_GGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_GGGG(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U2_GGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → MEMBER_IN_AG(Y, Visited)
MEMBER_IN_AG(X, .(H, L)) → U5_AG(X, H, L, member_in_ag(X, L))
MEMBER_IN_AG(X, .(H, L)) → MEMBER_IN_AG(X, L)
U3_GGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_GGGG(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U3_GGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → REACH_IN_AGGG(Y, Z, Edges, .(Y, Visited))
REACH_IN_AGGG(X, Y, Edges, Visited) → U1_AGGG(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_AGGG(X, Y, Edges, Visited) → MEMBER_IN_GG(.(X, .(Y, [])), Edges)
REACH_IN_AGGG(X, Z, Edges, Visited) → U2_AGGG(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_AGGG(X, Z, Edges, Visited) → MEMBER1_IN_GG(.(X, .(Y, [])), Edges)
U2_AGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_AGGG(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U2_AGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → MEMBER_IN_AG(Y, Visited)
U3_AGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_AGGG(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U3_AGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → REACH_IN_AGGG(Y, Z, Edges, .(Y, Visited))

The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x1, x2, x3, x4, x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x3, x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg(x1, x2)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x1, x3, x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x1, x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x2, x3, x4, x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x2, x3, x4, x5)
U2_GGGG(x1, x2, x3, x4, x5)  =  U2_GGGG(x1, x2, x3, x4, x5)
U6_GG(x1, x2, x3, x4)  =  U6_GG(x1, x3, x4)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)
MEMBER1_IN_GG(x1, x2)  =  MEMBER1_IN_GG(x1, x2)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
REACH_IN_GGGG(x1, x2, x3, x4)  =  REACH_IN_GGGG(x1, x2, x3, x4)
U1_GGGG(x1, x2, x3, x4, x5)  =  U1_GGGG(x1, x2, x3, x4, x5)
U3_GGGG(x1, x2, x3, x4, x5, x6)  =  U3_GGGG(x1, x2, x3, x4, x6)
U4_GGGG(x1, x2, x3, x4, x5)  =  U4_GGGG(x1, x2, x3, x4, x5)
U3_AGGG(x1, x2, x3, x4, x5, x6)  =  U3_AGGG(x2, x3, x4, x6)
U5_GG(x1, x2, x3, x4)  =  U5_GG(x1, x3, x4)
U4_AGGG(x1, x2, x3, x4, x5)  =  U4_AGGG(x2, x3, x4, x5)
U1_AGGG(x1, x2, x3, x4, x5)  =  U1_AGGG(x2, x3, x4, x5)
REACH_IN_AGGG(x1, x2, x3, x4)  =  REACH_IN_AGGG(x2, x3, x4)
U5_AG(x1, x2, x3, x4)  =  U5_AG(x3, x4)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 4 SCCs with 16 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_AG(X, .(H, L)) → MEMBER_IN_AG(X, L)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x1, x2, x3, x4, x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x3, x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg(x1, x2)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x1, x3, x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x1, x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x2, x3, x4, x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x2, x3, x4, x5)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_AG(X, .(H, L)) → MEMBER_IN_AG(X, L)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MEMBER_IN_AG(.(L)) → MEMBER_IN_AG(L)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER1_IN_GG(X, .(H, L)) → MEMBER1_IN_GG(X, L)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x1, x2, x3, x4, x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x3, x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg(x1, x2)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x1, x3, x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x1, x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x2, x3, x4, x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x2, x3, x4, x5)
MEMBER1_IN_GG(x1, x2)  =  MEMBER1_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER1_IN_GG(X, .(H, L)) → MEMBER1_IN_GG(X, L)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
MEMBER1_IN_GG(x1, x2)  =  MEMBER1_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MEMBER1_IN_GG(X, .(L)) → MEMBER1_IN_GG(X, L)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x1, x2, x3, x4, x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x3, x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg(x1, x2)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x1, x3, x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x1, x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x2, x3, x4, x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x2, x3, x4, x5)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(L)) → MEMBER_IN_GG(X, L)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

U3_AGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → REACH_IN_AGGG(Y, Z, Edges, .(Y, Visited))
REACH_IN_AGGG(X, Z, Edges, Visited) → U2_AGGG(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_AGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_AGGG(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))

The TRS R consists of the following rules:

reach_in_gggg(X, Y, Edges, Visited) → U1_gggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U5_gg(X, H, L, member_in_gg(X, L))
U5_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_gggg(X, Y, Edges, Visited)
reach_in_gggg(X, Z, Edges, Visited) → U2_gggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_gggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_gggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
reach_in_aggg(X, Y, Edges, Visited) → U1_aggg(X, Y, Edges, Visited, member_in_gg(.(X, .(Y, [])), Edges))
U1_aggg(X, Y, Edges, Visited, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_aggg(X, Y, Edges, Visited)
reach_in_aggg(X, Z, Edges, Visited) → U2_aggg(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_aggg(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_aggg(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))
U3_aggg(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → U4_aggg(X, Z, Edges, Visited, reach_in_aggg(Y, Z, Edges, .(Y, Visited)))
U4_aggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_aggg(X, Z, Edges, Visited)
U4_gggg(X, Z, Edges, Visited, reach_out_aggg(Y, Z, Edges, .(Y, Visited))) → reach_out_gggg(X, Z, Edges, Visited)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x1, x2, x3, x4, x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x3, x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x1, x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg(x1, x2)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x1, x3, x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x1, x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U4_gggg(x1, x2, x3, x4, x5)  =  U4_gggg(x1, x2, x3, x4, x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x2, x3, x4, x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg(x2, x3, x4)
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5)  =  U4_aggg(x2, x3, x4, x5)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
U3_AGGG(x1, x2, x3, x4, x5, x6)  =  U3_AGGG(x2, x3, x4, x6)
REACH_IN_AGGG(x1, x2, x3, x4)  =  REACH_IN_AGGG(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

U3_AGGG(X, Z, Edges, Visited, Y, member_out_ag(Y, Visited)) → REACH_IN_AGGG(Y, Z, Edges, .(Y, Visited))
REACH_IN_AGGG(X, Z, Edges, Visited) → U2_AGGG(X, Z, Edges, Visited, member1_in_gg(.(X, .(Y, [])), Edges))
U2_AGGG(X, Z, Edges, Visited, member1_out_gg(.(X, .(Y, [])), Edges)) → U3_AGGG(X, Z, Edges, Visited, Y, member_in_ag(Y, Visited))

The TRS R consists of the following rules:

member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U6_gg(X, H, L, member1_in_gg(X, L))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U5_ag(X, H, L, member_in_ag(X, L))
U6_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U5_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
[]  =  []
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg(x1, x2)
U6_gg(x1, x2, x3, x4)  =  U6_gg(x1, x3, x4)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
U3_AGGG(x1, x2, x3, x4, x5, x6)  =  U3_AGGG(x2, x3, x4, x6)
REACH_IN_AGGG(x1, x2, x3, x4)  =  REACH_IN_AGGG(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

REACH_IN_AGGG(Z, Edges, Visited) → U2_AGGG(Z, Edges, Visited, member1_in_gg(.(.([])), Edges))
U3_AGGG(Z, Edges, Visited, member_out_ag(Visited)) → REACH_IN_AGGG(Z, Edges, .(Visited))
U2_AGGG(Z, Edges, Visited, member1_out_gg(.(.([])), Edges)) → U3_AGGG(Z, Edges, Visited, member_in_ag(Visited))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg(H, .(L))
member1_in_gg(X, .(L)) → U6_gg(X, L, member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag(.(L))
member_in_ag(.(L)) → U5_ag(L, member_in_ag(L))
U6_gg(X, L, member1_out_gg(X, L)) → member1_out_gg(X, .(L))
U5_ag(L, member_out_ag(L)) → member_out_ag(.(L))

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule REACH_IN_AGGG(Z, Edges, Visited) → U2_AGGG(Z, Edges, Visited, member1_in_gg(.(.([])), Edges)) at position [3] we obtained the following new rules:

REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, member1_out_gg(.(.([])), .(x1)))
REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, U6_gg(.(.([])), x1, member1_in_gg(.(.([])), x1)))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, member1_out_gg(.(.([])), .(x1)))
U3_AGGG(Z, Edges, Visited, member_out_ag(Visited)) → REACH_IN_AGGG(Z, Edges, .(Visited))
U2_AGGG(Z, Edges, Visited, member1_out_gg(.(.([])), Edges)) → U3_AGGG(Z, Edges, Visited, member_in_ag(Visited))
REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, U6_gg(.(.([])), x1, member1_in_gg(.(.([])), x1)))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg(H, .(L))
member1_in_gg(X, .(L)) → U6_gg(X, L, member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag(.(L))
member_in_ag(.(L)) → U5_ag(L, member_in_ag(L))
U6_gg(X, L, member1_out_gg(X, L)) → member1_out_gg(X, .(L))
U5_ag(L, member_out_ag(L)) → member_out_ag(.(L))

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule U2_AGGG(Z, Edges, Visited, member1_out_gg(.(.([])), Edges)) → U3_AGGG(Z, Edges, Visited, member_in_ag(Visited)) at position [3] we obtained the following new rules:

U2_AGGG(y0, y1, .(x0), member1_out_gg(.(.([])), y1)) → U3_AGGG(y0, y1, .(x0), U5_ag(x0, member_in_ag(x0)))
U2_AGGG(y0, y1, .(x0), member1_out_gg(.(.([])), y1)) → U3_AGGG(y0, y1, .(x0), member_out_ag(.(x0)))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, member1_out_gg(.(.([])), .(x1)))
U2_AGGG(y0, y1, .(x0), member1_out_gg(.(.([])), y1)) → U3_AGGG(y0, y1, .(x0), U5_ag(x0, member_in_ag(x0)))
U3_AGGG(Z, Edges, Visited, member_out_ag(Visited)) → REACH_IN_AGGG(Z, Edges, .(Visited))
U2_AGGG(y0, y1, .(x0), member1_out_gg(.(.([])), y1)) → U3_AGGG(y0, y1, .(x0), member_out_ag(.(x0)))
REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, U6_gg(.(.([])), x1, member1_in_gg(.(.([])), x1)))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg(H, .(L))
member1_in_gg(X, .(L)) → U6_gg(X, L, member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag(.(L))
member_in_ag(.(L)) → U5_ag(L, member_in_ag(L))
U6_gg(X, L, member1_out_gg(X, L)) → member1_out_gg(X, .(L))
U5_ag(L, member_out_ag(L)) → member_out_ag(.(L))

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U3_AGGG(Z, Edges, Visited, member_out_ag(Visited)) → REACH_IN_AGGG(Z, Edges, .(Visited)) we obtained the following new rules:

U3_AGGG(z0, z1, .(z2), member_out_ag(.(z2))) → REACH_IN_AGGG(z0, z1, .(.(z2)))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, member1_out_gg(.(.([])), .(x1)))
U2_AGGG(y0, y1, .(x0), member1_out_gg(.(.([])), y1)) → U3_AGGG(y0, y1, .(x0), U5_ag(x0, member_in_ag(x0)))
U3_AGGG(z0, z1, .(z2), member_out_ag(.(z2))) → REACH_IN_AGGG(z0, z1, .(.(z2)))
U2_AGGG(y0, y1, .(x0), member1_out_gg(.(.([])), y1)) → U3_AGGG(y0, y1, .(x0), member_out_ag(.(x0)))
REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, U6_gg(.(.([])), x1, member1_in_gg(.(.([])), x1)))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg(H, .(L))
member1_in_gg(X, .(L)) → U6_gg(X, L, member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag(.(L))
member_in_ag(.(L)) → U5_ag(L, member_in_ag(L))
U6_gg(X, L, member1_out_gg(X, L)) → member1_out_gg(X, .(L))
U5_ag(L, member_out_ag(L)) → member_out_ag(.(L))

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, member1_out_gg(.(.([])), .(x1))) we obtained the following new rules:

REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), member1_out_gg(.(.([])), .(x1)))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U2_AGGG(y0, y1, .(x0), member1_out_gg(.(.([])), y1)) → U3_AGGG(y0, y1, .(x0), U5_ag(x0, member_in_ag(x0)))
U3_AGGG(z0, z1, .(z2), member_out_ag(.(z2))) → REACH_IN_AGGG(z0, z1, .(.(z2)))
REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), member1_out_gg(.(.([])), .(x1)))
U2_AGGG(y0, y1, .(x0), member1_out_gg(.(.([])), y1)) → U3_AGGG(y0, y1, .(x0), member_out_ag(.(x0)))
REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, U6_gg(.(.([])), x1, member1_in_gg(.(.([])), x1)))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg(H, .(L))
member1_in_gg(X, .(L)) → U6_gg(X, L, member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag(.(L))
member_in_ag(.(L)) → U5_ag(L, member_in_ag(L))
U6_gg(X, L, member1_out_gg(X, L)) → member1_out_gg(X, .(L))
U5_ag(L, member_out_ag(L)) → member_out_ag(.(L))

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule REACH_IN_AGGG(y0, .(x1), y2) → U2_AGGG(y0, .(x1), y2, U6_gg(.(.([])), x1, member1_in_gg(.(.([])), x1))) we obtained the following new rules:

REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), U6_gg(.(.([])), x1, member1_in_gg(.(.([])), x1)))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U2_AGGG(y0, y1, .(x0), member1_out_gg(.(.([])), y1)) → U3_AGGG(y0, y1, .(x0), U5_ag(x0, member_in_ag(x0)))
REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), U6_gg(.(.([])), x1, member1_in_gg(.(.([])), x1)))
U3_AGGG(z0, z1, .(z2), member_out_ag(.(z2))) → REACH_IN_AGGG(z0, z1, .(.(z2)))
REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), member1_out_gg(.(.([])), .(x1)))
U2_AGGG(y0, y1, .(x0), member1_out_gg(.(.([])), y1)) → U3_AGGG(y0, y1, .(x0), member_out_ag(.(x0)))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg(H, .(L))
member1_in_gg(X, .(L)) → U6_gg(X, L, member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag(.(L))
member_in_ag(.(L)) → U5_ag(L, member_in_ag(L))
U6_gg(X, L, member1_out_gg(X, L)) → member1_out_gg(X, .(L))
U5_ag(L, member_out_ag(L)) → member_out_ag(.(L))

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U2_AGGG(y0, y1, .(x0), member1_out_gg(.(.([])), y1)) → U3_AGGG(y0, y1, .(x0), U5_ag(x0, member_in_ag(x0))) we obtained the following new rules:

U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(z2)), U5_ag(.(z2), member_in_ag(.(z2))))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
                                              ↳ QDP
                                                ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(z2)), U5_ag(.(z2), member_in_ag(.(z2))))
REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), U6_gg(.(.([])), x1, member1_in_gg(.(.([])), x1)))
U3_AGGG(z0, z1, .(z2), member_out_ag(.(z2))) → REACH_IN_AGGG(z0, z1, .(.(z2)))
REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), member1_out_gg(.(.([])), .(x1)))
U2_AGGG(y0, y1, .(x0), member1_out_gg(.(.([])), y1)) → U3_AGGG(y0, y1, .(x0), member_out_ag(.(x0)))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg(H, .(L))
member1_in_gg(X, .(L)) → U6_gg(X, L, member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag(.(L))
member_in_ag(.(L)) → U5_ag(L, member_in_ag(L))
U6_gg(X, L, member1_out_gg(X, L)) → member1_out_gg(X, .(L))
U5_ag(L, member_out_ag(L)) → member_out_ag(.(L))

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U2_AGGG(y0, y1, .(x0), member1_out_gg(.(.([])), y1)) → U3_AGGG(y0, y1, .(x0), member_out_ag(.(x0))) we obtained the following new rules:

U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag(.(.(z2))))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
                                              ↳ QDP
                                                ↳ Instantiation
                                                  ↳ QDP
                                                    ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(z2)), U5_ag(.(z2), member_in_ag(.(z2))))
REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), U6_gg(.(.([])), x1, member1_in_gg(.(.([])), x1)))
U3_AGGG(z0, z1, .(z2), member_out_ag(.(z2))) → REACH_IN_AGGG(z0, z1, .(.(z2)))
REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), member1_out_gg(.(.([])), .(x1)))
U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag(.(.(z2))))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg(H, .(L))
member1_in_gg(X, .(L)) → U6_gg(X, L, member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag(.(L))
member_in_ag(.(L)) → U5_ag(L, member_in_ag(L))
U6_gg(X, L, member1_out_gg(X, L)) → member1_out_gg(X, .(L))
U5_ag(L, member_out_ag(L)) → member_out_ag(.(L))

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U3_AGGG(z0, z1, .(z2), member_out_ag(.(z2))) → REACH_IN_AGGG(z0, z1, .(.(z2))) we obtained the following new rules:

U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag(.(.(z2)))) → REACH_IN_AGGG(z0, .(z1), .(.(.(z2))))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
                                              ↳ QDP
                                                ↳ Instantiation
                                                  ↳ QDP
                                                    ↳ Instantiation
                                                      ↳ QDP
                                                        ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(z2)), U5_ag(.(z2), member_in_ag(.(z2))))
REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), U6_gg(.(.([])), x1, member1_in_gg(.(.([])), x1)))
U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag(.(.(z2)))) → REACH_IN_AGGG(z0, .(z1), .(.(.(z2))))
REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), member1_out_gg(.(.([])), .(x1)))
U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag(.(.(z2))))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg(H, .(L))
member1_in_gg(X, .(L)) → U6_gg(X, L, member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag(.(L))
member_in_ag(.(L)) → U5_ag(L, member_in_ag(L))
U6_gg(X, L, member1_out_gg(X, L)) → member1_out_gg(X, .(L))
U5_ag(L, member_out_ag(L)) → member_out_ag(.(L))

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), member1_out_gg(.(.([])), .(x1))) we obtained the following new rules:

REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg(.(.([])), .(z1)))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
                                              ↳ QDP
                                                ↳ Instantiation
                                                  ↳ QDP
                                                    ↳ Instantiation
                                                      ↳ QDP
                                                        ↳ Instantiation
                                                          ↳ QDP
                                                            ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(z2)), U5_ag(.(z2), member_in_ag(.(z2))))
REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), U6_gg(.(.([])), x1, member1_in_gg(.(.([])), x1)))
U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag(.(.(z2)))) → REACH_IN_AGGG(z0, .(z1), .(.(.(z2))))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg(.(.([])), .(z1)))
U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag(.(.(z2))))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg(H, .(L))
member1_in_gg(X, .(L)) → U6_gg(X, L, member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag(.(L))
member_in_ag(.(L)) → U5_ag(L, member_in_ag(L))
U6_gg(X, L, member1_out_gg(X, L)) → member1_out_gg(X, .(L))
U5_ag(L, member_out_ag(L)) → member_out_ag(.(L))

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule REACH_IN_AGGG(z0, .(x1), .(.(z2))) → U2_AGGG(z0, .(x1), .(.(z2)), U6_gg(.(.([])), x1, member1_in_gg(.(.([])), x1))) we obtained the following new rules:

REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), U6_gg(.(.([])), z1, member1_in_gg(.(.([])), z1)))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
                                              ↳ QDP
                                                ↳ Instantiation
                                                  ↳ QDP
                                                    ↳ Instantiation
                                                      ↳ QDP
                                                        ↳ Instantiation
                                                          ↳ QDP
                                                            ↳ Instantiation
                                                              ↳ QDP
                                                                ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(z2)), U5_ag(.(z2), member_in_ag(.(z2))))
U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag(.(.(z2)))) → REACH_IN_AGGG(z0, .(z1), .(.(.(z2))))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg(.(.([])), .(z1)))
U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag(.(.(z2))))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), U6_gg(.(.([])), z1, member1_in_gg(.(.([])), z1)))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg(H, .(L))
member1_in_gg(X, .(L)) → U6_gg(X, L, member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag(.(L))
member_in_ag(.(L)) → U5_ag(L, member_in_ag(L))
U6_gg(X, L, member1_out_gg(X, L)) → member1_out_gg(X, .(L))
U5_ag(L, member_out_ag(L)) → member_out_ag(.(L))

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(z2)), U5_ag(.(z2), member_in_ag(.(z2)))) we obtained the following new rules:

U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(.(z2))), U5_ag(.(.(z2)), member_in_ag(.(.(z2)))))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
                                              ↳ QDP
                                                ↳ Instantiation
                                                  ↳ QDP
                                                    ↳ Instantiation
                                                      ↳ QDP
                                                        ↳ Instantiation
                                                          ↳ QDP
                                                            ↳ Instantiation
                                                              ↳ QDP
                                                                ↳ Instantiation
                                                                  ↳ QDP
                                                                    ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag(.(.(z2)))) → REACH_IN_AGGG(z0, .(z1), .(.(.(z2))))
U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(.(z2))), U5_ag(.(.(z2)), member_in_ag(.(.(z2)))))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg(.(.([])), .(z1)))
U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag(.(.(z2))))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), U6_gg(.(.([])), z1, member1_in_gg(.(.([])), z1)))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg(H, .(L))
member1_in_gg(X, .(L)) → U6_gg(X, L, member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag(.(L))
member_in_ag(.(L)) → U5_ag(L, member_in_ag(L))
U6_gg(X, L, member1_out_gg(X, L)) → member1_out_gg(X, .(L))
U5_ag(L, member_out_ag(L)) → member_out_ag(.(L))

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1)

We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule U2_AGGG(z0, .(z1), .(.(z2)), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag(.(.(z2)))) we obtained the following new rules:

U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(.(z2))), member_out_ag(.(.(.(z2)))))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ Instantiation
                                  ↳ QDP
                                    ↳ Instantiation
                                      ↳ QDP
                                        ↳ Instantiation
                                          ↳ QDP
                                            ↳ Instantiation
                                              ↳ QDP
                                                ↳ Instantiation
                                                  ↳ QDP
                                                    ↳ Instantiation
                                                      ↳ QDP
                                                        ↳ Instantiation
                                                          ↳ QDP
                                                            ↳ Instantiation
                                                              ↳ QDP
                                                                ↳ Instantiation
                                                                  ↳ QDP
                                                                    ↳ Instantiation
                                                                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

U3_AGGG(z0, .(z1), .(.(z2)), member_out_ag(.(.(z2)))) → REACH_IN_AGGG(z0, .(z1), .(.(.(z2))))
U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(.(z2))), member_out_ag(.(.(.(z2)))))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg(.(.([])), .(z1)))
U2_AGGG(z0, .(z1), .(.(.(z2))), member1_out_gg(.(.([])), .(z1))) → U3_AGGG(z0, .(z1), .(.(.(z2))), U5_ag(.(.(z2)), member_in_ag(.(.(z2)))))
REACH_IN_AGGG(z0, .(z1), .(.(.(z2)))) → U2_AGGG(z0, .(z1), .(.(.(z2))), U6_gg(.(.([])), z1, member1_in_gg(.(.([])), z1)))

The TRS R consists of the following rules:

member1_in_gg(H, .(L)) → member1_out_gg(H, .(L))
member1_in_gg(X, .(L)) → U6_gg(X, L, member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag(.(L))
member_in_ag(.(L)) → U5_ag(L, member_in_ag(L))
U6_gg(X, L, member1_out_gg(X, L)) → member1_out_gg(X, .(L))
U5_ag(L, member_out_ag(L)) → member_out_ag(.(L))

The set Q consists of the following terms:

member1_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1)

We have to consider all (P,Q,R)-chains.